FDL - Nuprl Definition : fpf-val

Nuprl Definition : fpf-val

z != f(x)

P(a;z) == (

x

dom(f))

P(x;f(x))

clarification:

fpf-val(eq; f; x; a,z.P(a;z)) == (

fpf-dom(eq; x; f))

P(x;feq(x))

Definitions f(x), x dom(f), b, P Q

FDL editor aliases fpf-val